half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
↳ QTRS
↳ DependencyPairsProof
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
LOGITER(x, y) → HALF(x)
LOGITER(x, y) → LE(s(0), x)
LOGARITHM(x) → LOGITER(x, 0)
HALF(s(s(x))) → HALF(x)
LOGITER(x, y) → LE(s(s(0)), x)
INC(s(x)) → INC(x)
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(x, y) → INC(y)
LE(s(x), s(y)) → LE(x, y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
LOGITER(x, y) → HALF(x)
LOGITER(x, y) → LE(s(0), x)
LOGARITHM(x) → LOGITER(x, 0)
HALF(s(s(x))) → HALF(x)
LOGITER(x, y) → LE(s(s(0)), x)
INC(s(x)) → INC(x)
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(x, y) → INC(y)
LE(s(x), s(y)) → LE(x, y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
INC(s(x)) → INC(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
INC(s(x)) → INC(x)
The value of delta used in the strict ordering is 1/16.
POL(INC(x1)) = (1/4)x_1
POL(s(x1)) = 1/4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
LE(s(x), s(y)) → LE(x, y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LE(s(x), s(y)) → LE(x, y)
The value of delta used in the strict ordering is 1.
POL(s(x1)) = 1 + x_1
POL(LE(x1, x2)) = x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
HALF(s(s(x))) → HALF(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HALF(s(s(x))) → HALF(x)
The value of delta used in the strict ordering is 3/8.
POL(HALF(x1)) = (1/2)x_1
POL(s(x1)) = 1/4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h